Termination w.r.t. Q proof of /tmp/tmpMLgVAp/4.51.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

k(x, h(x), a) → h(x)

Used ordering:
Polynomial interpretation [25]:

POL(a) = 2
POL(f(x₁)) = x₁
POL(g(x₁)) = x₁
POL(h(x₁)) = x₁
POL(k(x₁, x₂, x₃)) = x₁ + x₂ + x₃

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(f(x), y, x) → f(x)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(f(x), y, x) → f(x)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

k(f(x), y, x) → f(x)

Used ordering:
Polynomial interpretation [25]:

POL(a) = 0
POL(f(x₁)) = x₁
POL(g(x₁)) = 2·x₁
POL(h(x₁)) = x₁
POL(k(x₁, x₂, x₃)) = 1 + 2·x₁ + x₂ + 2·x₃

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ Overlay + Local Confluence

            ↳ QTRS

              ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(a) → H(a)
H(g(x)) → H(f(x))
H(g(x)) → F(x)

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ Overlay + Local Confluence

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(a) → H(a)
H(g(x)) → H(f(x))
H(g(x)) → F(x)

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ Overlay + Local Confluence

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

f(a) → g(h(a))
h(g(x)) → g(h(f(x)))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ Overlay + Local Confluence

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ UsableRulesProof

                        ↳ QDP

                          ↳ RFCMatchBoundsDPProof

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

f(a) → g(h(a))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

H(g(x)) → H(f(x))

To find matches we regarded all rules of R and P:

f(a) → g(h(a))
H(g(x)) → H(f(x))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

40, 41, 42, 43, 44, 45

Node 40 is start node and node 41 is final node.

Those nodes are connect through the following edges:

40 to 42 labelled H_1(0)
40 to 45 labelled H_1(1)
41 to 41 labelled #_1(0)
42 to 41 labelled f_1(0)
42 to 43 labelled g_1(1)
43 to 44 labelled h_1(1)
44 to 41 labelled a(1)
45 to 43 labelled f_1(1)